Library isotomic_conjugate

Require Export PointsType.
Require Import TrianglesDefs.
Require Import midpoint.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition isotomic_conjugate P :=
 match P with
  cTriple p q r ⇒
  cTriple (1/(p×a^2)) (1/(q×b^2)) (1/(r×c^2))
 end.

Lemma isotomic_conjugate_property :
 ∀ P,
   is_not_on_sidelines P →
   match cevian_triangle P with
     (A1,B1,C1) ⇒
   match cevian_triangle (isotomic_conjugate P) with
     (A2,B2,C2) ⇒ eq_points (midpoint pointA pointB) (midpoint C1 C2)
   end
end.
Proof.
intros.
destruct P.
unfold cevian_triangle, isotomic_conjugate, eq_points, midpoint.
simpl in ×.
decompose [and] H.
split;field;
repeat split;
auto with triangle_hyps.
Qed.

Lemma isotomic_involution : ∀ P,
 is_not_on_sidelines P →
 eq_points (isotomic_conjugate (isotomic_conjugate P)) P.
Proof.
intros.
destruct P.
unfold is_not_on_sidelines in ×.
unfold eq_points;simpl.
decompose [and] H.
split;field;auto with triangle_hyps.
Qed.

End Triangle.